Nuprl Lemma : vartype-es-type
0,22
postcript
pdf
es
:ES,
i
,
x
:Id,
T
:Type. vartype(
i
;
x
)
T
@
i
x
has type
T
latex
Definitions
@
i
x
has type
T
,
e
@
i
.
P
(
e
)
,
P
Q
,
P
&
Q
,
Prop
,
loc(
e
)
,
E
,
x
when
e
,
(
x
after
e
)
,
vartype(
i
;
x
)
,
x
:
A
.
B
(
x
)
,
Id
,
ES
,
T
,
True
,
t
T
Lemmas
event
system
wf
,
Id
wf
,
true
wf
,
squash
wf
,
es-vartype
wf
,
subtype
rel
wf
,
es-after
wf
,
es-when
wf
,
es-E
wf
,
es-loc
wf
origin
es:ES, i, x:Id, T:Type. vartype(i;x) 
T 
@i x has type T es:ES, i, x:Id, T:Type. vartype(i;x) T @i x has type T e@i. P(e) Qx:A. B(x)
T
T